# Exercise 1

We should derive a resolution proof, we begin with the origin formula and reformulate it to have simpler terms.
We will assume the premise and the negation of the conclusion.

$$
\begin{aligned}
\varphi &= (x \oplus y) \land (y \leftrightarrow z) \land \neg (x \land z) \\
&= (x \lor y) \land \neg (x \land y) \land ((y \land z) \lor (\neg y \land \neg z)) \land (\neg x \lor \neg z) \\
&= (x \lor y) \land (\neg x \lor \neg y) \land ((y \land z) \lor (\neg y \land \neg z)) \land (\neg x \lor \neg z) \\
&= (x \lor y) \land (\neg x \lor \neg y) \land (\neg y \lor z) \land (y \lor \neg z) \land (\neg x \lor \neg z) \\
\end{aligned}
$$

Our result is a DNF formula.

We add the blocking clauses now:

$$
\begin{aligned}
\varphi_{blocked} &= (x \lor y) \land (\neg x \lor \neg y) \land (\neg y \lor z) \land (y \lor \neg z) \land (\neg x \lor \neg z) \land \neg (\neg x \land y \land z) \land \neg (x \land \neg y \land \neg z) \\
&= (x \lor y) \land (\neg x \lor \neg y) \land (\neg y \lor z) \land (y \lor \neg z) \land (\neg x \lor \neg z) \land (x \lor \neg y \lor \neg z) \land (\neg x \lor y \lor z) \\
&= C_1 \land C_2 \land C_3 \land C_4 \land C_5 \land C_6 \land C_7 \\
\end{aligned}
$$

We can begin the resolution now:

$$
\begin{aligned}
r_1 = R(C_1, C_6, y) &= x \lor x \lor \neg z = x \lor \neg z \\
r_2 = R(r_1, C_5, x) &= \neg z \lor \neg z = \neg z \\
r_3 = R(C_2, C_7, y) &= \neg x \lor \neg x \lor z = \neg x \lor z \\
r_4 = R(r_3, C_5, z) &= \neg x \lor \neg x = \neg x \\
r_5 = R(r_2, C_3, z) &= \neg y \\
r_6 = R(r_4, C_1, x) &= y \\
r_7 = R(r_5, r_6, x) &= \square \\
\end{aligned}
$$

This concludes our proof.
Do note that we have performend the factorization steps immediately to shorten the proof.

# Exercise 2

For exercise 2, we check whether the use of bit-vector arithmetic might lead to some problems.
For subtask 1, this is indeed the case, we can give a counterexample that fulfills our premises, but not the conclusion:

```
  (define-fun h () (_ BitVec 64)
    #x7fcfffffffffffff)
  (define-fun l () (_ BitVec 64)
    #x00b0000000000001)
  (define-fun m () (_ BitVec 64)
    #xc040000000000000)
```

For subtask 2, we test again for validity by trying to find a counterexample.
This time z3 returns unsat, so we know that the formula is valid in the theory of integers.

For subtask 3, we apply a new and improved statement and indeed we find that it works.

# Exercise 3

### Subtask 1

This formula is unsatisfiable and using z3 we can find the unsatisfiable core to be $x \dot= y \land z \dot= G(F(y)) \land z \dot\neq G(F(x))$.
So for the following analysis we can restrict ourselves to this core.

We retrieve a semantic argument proof first:

$$
\begin{aligned}
(premise) & & I &\vDash x \dot= y \land z \dot= G(F(y)) \land z \dot\neq G(F(x)) & & premise \\
(1) & & I &\vDash x \dot= y & & premise, and \\
(2) & & I &\vDash z \dot= G(F(y)) & & premise, and \\
(3) & & I &\vDash z \dot\neq G(F(x)) & & premise, and \\
(4) & & I &\vDash x \dot= y \rightarrow G(F(x)) \dot= G(F(y)) & & functional\ congruence \\
(5) & & I &\vDash G(F(x)) \dot= G(F(y)) & & 1, 4, MP \\
(6) & & I &\vDash z \dot= G(F(x)) & & 2, 5, transitivity \\
(7) & & I &\vDash \bot & & 3, 6 \\
\end{aligned}
$$

So we find out, if we have the axiom of functional congruence and the axiom of transitivity, then this formula cannot be satisfiable.

### Subtask 2

For subtask 2 we should develop a satisfiability-preserving (not necessarily validity-preserving!) variant of Ackermann's reduction.
For this task, we choose the same approach as the variant we have already proven as a homework in the lecture.

We know that the end result of Ackermann's reduction is the following:

$$
\varphi^{EUF}\text{ is valid iff }FC^E(\varphi^{EUF}) \rightarrow flat^E(\varphi^{EUF})\text{ is valid}
$$

Thus we can work from this as a base, using $FC^E(\varphi^{EUF})$ and $flat^E(\varphi^{EUF})$ we get from the transformations in Ackermann's reduction:

$$
\begin{aligned}
\neg \varphi^{EUF}\text{ is not valid }&\text{ iff}&FC^E(\neg \varphi^{EUF}) \rightarrow flat^E(\neg \varphi^{EUF})&\text{ is not valid} \\
\varphi^{EUF}\text{ is sat }&\text{ iff}&\neg FC^E(\neg \varphi^{EUF}) \lor flat^E(\neg \varphi^{EUF})&\text{ is not valid} \\
&\text{ iff}&\neg FC^E(\neg \varphi^{EUF}) \lor flat^E(\neg \varphi^{EUF})&\text{ is not valid} \\
&\text{ iff}&\neg \neg (\neg FC^E(\neg \varphi^{EUF}) \lor flat^E(\neg \varphi^{EUF}))&\text{ is not valid} \\
&\text{ iff}&\neg (\neg FC^E(\neg \varphi^{EUF}) \lor flat^E(\neg \varphi^{EUF}))&\text{ is sat} \\
&\text{ iff}&FC^E(\neg \varphi^{EUF}) \land \neg flat^E(\neg \varphi^{EUF})&\text{ is sat} \\
&\text{ iff}&FC^E(\neg \varphi^{EUF}) \land flat^E(\varphi^{EUF})&\text{ is sat} \\
\varphi^{EUF}\text{ is sat }&\text{ iff}&FC^E(\varphi^{EUF}) \land flat^E(\varphi^{EUF})&\text{ is sat} \\
\end{aligned}
$$

Do note that we used the following facts:

$$
\neg flat^E(\neg \varphi^{EUF}) = flat^E(\varphi^{EUF})\text{\ \ \ and\ \ \ }FC^E(\neg \varphi^{EUF}) = FC^E(\varphi^{EUF})
$$

Now we can translate our given formula to $FC^E(\varphi^{EUF})$ and $flat^E(\varphi^{EUF})$:

$$
flat^E(\varphi^{EUF}):\ x \dot= y \land f_{x} \dot= g_{gy} \land z \dot= g_{fy} \land z \dot\neq g_{fx}
$$

$$
\begin{aligned}
FC^E(\varphi^{EUF}):\ 
&x \dot= y \rightarrow f_{x} \dot= f_{y} \land \\
&y \dot= g_{y} \rightarrow g_{y} \dot= g_{gy} \land \\
&y \dot= f_{x} \rightarrow g_{y} \dot= g_{fx} \land \\
&y \dot= f_{y} \rightarrow g_{y} \dot= g_{fy} \land \\
&f_{x} \dot= f_{y} \rightarrow g_{fx} \dot= g_{fy} \land \\
&g_{y} \dot= f_{x} \rightarrow g_{gy} \dot= g_{fx} \land \\
&g_{y} \dot= f_{y} \rightarrow g_{gy} \dot= g_{fy} \land \\
\end{aligned}
$$

And in the next step, we check for (un-)satisfiability of the translated formula $\varphi^E = FC^E(\varphi^{EUF}) \land flat^E(\varphi^{EUF})$.

Using z3 we find as before that the reduced formula is still unsatisfiable!

### Subtask 3

For this subtask we can attempt to remove individual functional constraints, which we name `F[1-7]` as they appear in the $FC^E(\varphi^{EUF})$ formula above

What we find is that removing any of the constraints other than `F1` and `F5` keeps the formula unsatisfiable, while removing either `F1` or `F5` changes the logical status to satisfiable.
Indeed we can remove all constraints except for `F1` and `F5` and the formula remains unsatisfiable, until we remove either one of the remaining two.

Thus we can infer that the reduced formula has the least possible functional constraints:

$$
\varphi^E_{M} = FC^E_{M}(\varphi^{EUF}) \land flat^E(\varphi^{EUF})
$$

$$
\begin{aligned}
FC^E_{M}(\varphi^{EUF}):\ 
&x \dot= y \rightarrow f_{x} \dot= f_{y} \land \\
&f_{x} \dot= f_{y} \rightarrow g_{fx} \dot= g_{fy} \land \\
\end{aligned}
$$

This makes sense, as one can easily see that the functional equivalence coupled with the fact that $z$ is both equal and unequal to the functional results results in unsatisfiable.

### Subtask 4

The result of the `(get-unsat-core)` command in z3 actually yields the same result, with `(F1 F5)` (equivalent to $FC^E_{M}(\varphi^{EUF})$) being the unsat core, so we could have arrived at this conclusion much faster.

# Exercise 4

In subtask 1 we check $\varphi$ and find out that it is not valid, i.e., a counterexample exists.

For subtask 2, after we added our new quantified axiom of commutativity, the formula becomes valid.
Retrieving an unsat core tells us that all assumptions are necessary for validity.

# Exercise 5

In this task we find that the first two formulas are not valid because counterexamples can be found, but the latter two are valid.

We retrieve a semantic argument method proof first for subtask 3:

$$
\begin{aligned}
(premise) & & I &\vDash a \langle i \triangleleft e \rangle [j] {\dot=} e & premise \\
(conclusion) & & I &\nvDash i \dot= j \lor a[j] \dot= e & conclusion \\
(1) & & I &\nvDash i \dot= j & conclusion, and \\
(2) & & I &\nvDash a[j] \dot= e & conclusion, and \\
(3) & & I &\vDash i \dot\neq j \rightarrow a \langle i \triangleleft e \rangle [j] \dot= a[j] & ROW2, (a, v, i, j) \to (a, e, i, j) \\
(4) & & I &\vDash i \dot\neq j & 1, not \\
(5) & & I &\vDash a \langle i \triangleleft e \rangle [j] \dot= a[j] & 3, 4, MP \\
(6) & & I &\vDash a[j] \dot= e & premise, 5, transitivity \\
(7) & & I &\vDash \bot & 2, 6 \\
\end{aligned}
$$

Thus we have confirmed the practical result we got using z3.

We will do the same for subtask 4:

$$
\begin{aligned}
(premise) & & I &\vDash a \langle i \triangleleft e \rangle \langle j \triangleleft f \rangle [k] {\dot=} g \land j \not= k \land i = j & premise \\
(conclusion) & & I &\nvDash a[k] = g & conclusion \\
(1) & & I &\vDash a \langle i \triangleleft e \rangle \langle j \triangleleft f \rangle [k] {\dot=} g & premise, and \\
(2) & & I &\vDash j \not= k & premise, and \\
(3) & & I &\vDash i = j & premise, and \\
(4) & & I &\vDash j \dot\neq k \rightarrow a \langle i \triangleleft e \rangle \langle j \triangleleft f \rangle [k] \dot= a[k] & ROW2, (a, v, i, j) \to (a \langle i \triangleleft e \rangle, f, j, k) \\
(4) & & I &\vDash a \langle i \triangleleft e \rangle \langle j \triangleleft f \rangle [k] \dot= a[k] & 2, 4, MP \\
(5) & & I &\vDash a[k] = g & 1, 2, transitivity \\
(6) & & I &\vDash \bot & conclusion, 5 \\
\end{aligned}
$$

Thus we have confirmed another practical result we got using z3.

# Exercise 6

Using z3 with the supplied `all_smt` method we get the following result:

```
for n=2 there are 670 models
for n=3 there are 55252 models
```

Sadly, finding the models for $n=4$ is computationally expensive and takes too much time.

# Exercise 7

For exercise 7, if we turn up z3 it will tell us that the negation of the conclusion (the result of `avgu` not being equal to the requested value $\lfloor \frac{x + y}{2} \rfloor$) is impossible or unsat, in which case the implementation for `avgu` would be invalid.

In the C standard, when two operators of a shift right operation are signed numbers, arithmetic right shifts are used.
Similarly for unsigned operators, logical right shifts are used.
This is a natural convention and helps us out here, had the shift operation been specified to be arithmetic, then the implementation would not be valid!

For arithmetic right shift, we can find the following counterexample:

```
  (define-fun avgu () (_ BitVec 8)
    #xfe)
  (define-fun y () (_ BitVec 8)
    #x23)
  (define-fun x () (_ BitVec 8)
    #xd9)
  (define-fun realavg () Int
    126)
```

But for logical right shift, the assertion that the returned values of `avgu` is equal to the requested value is valid.
Because the C standard favors the use of a logical right shift, we can conclude that the implementation of `avgu` is valid.

# Exercise 8

For this exercise, we want to pack 6 elements of different weight to get a total weight of *exactly* 16.00 kg.
For this problem, as all weights are reals with two decimal points, we will consider the weights as integers by scaling the reals by a factor of 100.
This operation doesn't change the space of possible correct results.
Similarly to exercise 6, we use the `all_smt` method to exhaust the search space.

We get as a result two possible assignments:

```
[g_1 = 3, g_5 = 0, g_0 = 0, g_3 = 1, g_4 = 1, g_2 = 0]
where 0 + 0*240 + 3*275 + 0*335 + 1*355 + 1*420 + 0*580 == 1600
[g_2 = 3, g_5 = 0, g_0 = 1, g_3 = 1, g_4 = 0, g_1 = 0]
where 0 + 1*240 + 0*275 + 3*335 + 1*355 + 0*420 + 0*580 == 1600
```
